DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2020.29

Semi-Axiomatic Sequent Calculus

Authors: Henry DeYoung, Frank Pfenning, and Klaas Pruiksma

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

We present the semi-axiomatic sequent calculus (SAX) that blends features of Gentzen’s sequent calculus with an axiomatic formulation of intuitionistic logic. We develop and prove a suitable analogue to cut elimination and then show that a natural computational interpretation of SAX provides a simple form of shared memory concurrency.

Cite as

Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-Axiomatic Sequent Calculus. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{deyoung_et_al:LIPIcs.FSCD.2020.29,
  author =	{DeYoung, Henry and Pfenning, Frank and Pruiksma, Klaas},
  title =	{{Semi-Axiomatic Sequent Calculus}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.29},
  URN =		{urn:nbn:de:0030-drops-123515},
  doi =		{10.4230/LIPIcs.FSCD.2020.29},
  annote =	{Keywords: Sequent calculus, Curry-Howard isomorphism, shared memory concurrency}
}

Document

DOI: 10.4230/LIPIcs.CSL.2012.228

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication

Authors: Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract

Prior work has shown that intuitionistic linear logic can be seen as a session-type discipline for the pi-calculus, where cut reduction in the sequent calculus corresponds to synchronous process reduction. In this paper, we exhibit a new process assignment from the asynchronous, polyadic pi-calculus to exactly the same proof rules. Proof-theoretically, the difference between these interpretations can be understood through permutations of inference rules that preserve observational equivalence of closed processes in the synchronous case. We also show that, under this new asynchronous interpretation, cut reductions correspond to a natural asynchronous buffered session semantics, where each session is allocated a separate communication buffer.

Cite as

Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 228-242, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{deyoung_et_al:LIPIcs.CSL.2012.228,
  author =	{DeYoung, Henry and Caires, Lu{\'\i}s and Pfenning, Frank and Toninho, Bernardo},
  title =	{{Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{228--242},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.228},
  URN =		{urn:nbn:de:0030-drops-36753},
  doi =		{10.4230/LIPIcs.CSL.2012.228},
  annote =	{Keywords: linear logic, cut reduction, asynchronous pi-calculus, session types}
}

Search Results

Documents authored by DeYoung, Henry

Semi-Axiomatic Sequent Calculus

Abstract

Cite as

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication

Abstract

Cite as

Thanks for your feedback!

Could not send message